Curry-Howard correspondence
#complexity_theory #type_theory #PLT
#incomplete
intuition: relationship between computer programs and proofs
See also
- relationship between type theory and category theory
References
- https://en.wikipedia.org/wiki/Curry–Howard_correspondence
- https://ncatlab.org/nlab/show/propositions+as+types
- https://web2.qatar.cmu.edu/cs/15317/lectures/04-curryhoward.pdf
- https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html
- https://math.stackexchange.com/questions/166430/curry-howard-correspondence
- https://www.pls-lab.org/Classical_Curry-Howard
- https://en.wikipedia.org/wiki/Fragment_(logic)